FDL - Step of Proof: fast-fib-opt

Step of Proof: fast-fib-opt

Inference at *
Iof proof for Lemma fast-fib-opt:

n:

. {m:

| m = fib(n)}

by (Id)

CollapseTHEN (optimize_extract (ioid Obid: fast-fib) LinearC)

C1:

C1:

TERMOF{fast-fib:ObjectId, \\v:l}

(

n:

. {m:

| m = fib(n)} )

C.

Definitions fast-fib, t T

Lemmas fast-fib